Definitions | t T, P  Q, x:A. B(x), P & Q, A & B, mval(m), val(e), valtype(e), msgtype(m), (e < e'), mtag(m), tag(e), Id, lnk(e), IdLnk, isrcv(e), b, Prop, x:A. B(x), e:rvc(l,tg,v).P(e;v), A B, i j < k, {i..j }, ||as||, False, A, , E, (Msg on l), Msg, S T, sends(l;e), l[i], (x l), ES, msg(l;t;v), index(e), True, T, SQType(T), Msg(M) |